$\forall$$A$, $B$:Type. ($\exists$$f$:$A$$\rightarrow$$B$. Bij($A$;$B$;$f$)) $\Leftarrow\!\Rightarrow$ 1{-}1{-}Corresp($A$;$B$)